\begin{tabbing}
fpf{-}compatible($A$; $a$.$B$($a$); ${\it eq}$; $f$; $g$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$x$:$A$. \+
\\[0ex](($\uparrow$fpf{-}dom(${\it eq}$; $x$; $f$)) $\wedge$ ($\uparrow$fpf{-}dom(${\it eq}$; $x$; $g$)))
\\[0ex]$\Rightarrow$ (fpf{-}ap($f$; ${\it eq}$; $x$) = fpf{-}ap($g$; ${\it eq}$; $x$))
\-
\end{tabbing}